| 1. Identificação | |
| Tipo de Referência | Artigo em Revista Científica (Journal Article) |
| Site | plutao.sid.inpe.br |
| Código do Detentor | isadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S |
| Identificador | 8JMKD3MGP3W/3GDQJBB |
| Repositório | sid.inpe.br/plutao/2014/06.03.21.33 (acesso restrito) |
| Última Atualização | 2014:09.11.12.33.09 (UTC) administrator |
| Repositório de Metadados | sid.inpe.br/plutao/2014/06.03.21.33.44 |
| Última Atualização dos Metadados | 2022:03.17.16.24.02 (UTC) administrator |
| DOI | 10.4204/EPTCS.147.10 |
| ISSN | 2075-2180 |
| Rótulo | lattes: 5039690360728170 2 BrasilRebelodosSantosAlexLank:2014:TrUMBe |
| Chave de Citação | SantosSantVija:2014:TrUMBe |
| Título | Transformation of UML behavioral diagrams to support software model checking  |
| Projeto | FINEP (01.10.0233.00); FAPESP (2012/23767-2). |
| Ano | 2014 |
| Data de Acesso | 29 abr. 2024 |
| Tipo de Trabalho | journal article |
| Tipo Secundário | PRE PI |
| Número de Arquivos | 1 |
| Tamanho | 338 KiB |
| 2. Contextualização | |
| Autor | 1 Santos, Luciana Brasil Rebelo dos 2 Santiago Júnior, Valdivino Alexandre de 3 Vijaykumar, Nandamudi Lankalapalli |
| Identificador de Curriculo | 1 2 8JMKD3MGP5W/3C9JJB5 3 8JMKD3MGP5W/3C9JHTU |
| Grupo | 1 CAP-COMP-SPG-INPE-MCTI-GOV-BR 2 CEA-CEA-INPE-MCTI-GOV-BR 3 LAC-CTE-INPE-MCTI-GOV-BR |
| Afiliação | 1 Instituto Nacional de Pesquisas Espaciais (INPE) 2 Instituto Nacional de Pesquisas Espaciais (INPE) 3 Instituto Nacional de Pesquisas Espaciais (INPE) |
| Endereço de e-Mail do Autor | 1 luciana.santos@lac.inpe.br 2 valdivino.santiago@inpe.br 3 vijay.nl@inpe.br |
| Endereço de e-Mail | marcelo.pazos@inpe.br |
| Revista | Electronic Proceedings in Theoretical Computer Science |
| Volume | 147 |
| Páginas | 133-142 |
| Nota Secundária | B5_CIÊNCIA_DA_COMPUTAÇÃO B5_ENGENHARIAS_IV C_FILOSOFIA/TEOLOGIA:subcomissão_FILOSOFIA |
| Histórico (UTC) | 2014-06-03 22:25:45 :: lattes -> administrator :: 2014 2022-03-17 16:24:02 :: administrator -> marcelo.pazos@inpe.br :: 2014 |
| 3. Conteúdo e estrutura | |
| É a matriz ou uma cópia? | é a matriz |
| Estágio do Conteúdo | concluido |
| Transferível | 1 |
| Tipo do Conteúdo | External Contribution |
| Tipo de Versão | publisher |
| Palavras-Chave | model checking UML verification and validation |
| Resumo | Unified Modeling Language (UML) is currently accepted as the standard for modeling (objectoriented) software, and its use is increasing in the aerospace industry. Verification and Validation of complex software developed according to UML is not trivial due to complexity of the software itself, and the several different UML models/diagrams that can be used to model behavior and structure of the software. This paper presents an approach to transform up to three different UML behavioral diagrams (sequence, behavioral state machines, and activity) into a single Transition System to support Model Checking of software developed in accordance with UML. In our approach, properties are formalized based on use case descriptions. The transformation is done for the NuSMV model checker, but we see the possibility in using other model checkers, such as SPIN. The main contribution of our work is the transformation of a non-formal language (UML) to a formal language (language of the NuSMV model checker) towards a greater adoption in practice of formal methods in software development. |
| Área | COMP |
| Arranjo 1 | urlib.net > BDMCI > Fonds > Produção anterior à 2021 > LABAC > Transformation of UML... |
| Arranjo 2 | urlib.net > BDMCI > Fonds > Produção anterior à 2021 > CGCEA > Transformation of UML... |
| Arranjo 3 | urlib.net > BDMCI > Fonds > Produção pgr ATUAIS > CAP > Transformation of UML... |
| Conteúdo da Pasta doc | acessar |
| Conteúdo da Pasta source | não têm arquivos |
| Conteúdo da Pasta agreement | não têm arquivos |
| 4. Condições de acesso e uso | |
| Idioma | en |
| Arquivo Alvo | 1404.0855v1.pdf |
| Grupo de Usuários | lattes marcelo.pazos@inpe.br |
| Grupo de Leitores | administrator marcelo.pazos@inpe.br |
| Visibilidade | shown |
| Permissão de Leitura | deny from all and allow from 150.163 |
| Permissão de Atualização | não transferida |
| 5. Fontes relacionadas | |
| Repositório Espelho | iconet.com.br/banon/2006/11.26.21.31 |
| Unidades Imediatamente Superiores | 8JMKD3MGPCW/3ESGTTP 8JMKD3MGPCW/3EU2FR5 8JMKD3MGPCW/3F2PHGS |
| Lista de Itens Citando | sid.inpe.br/bibdigital/2013/10.01.23.29 2 sid.inpe.br/bibdigital/2013/09.22.23.14 2 sid.inpe.br/mtc-m21/2012/07.13.15.01.24 1 |
| Divulgação | WEBSCI; PORTALCAPES; COMPENDEX. |
| Acervo Hospedeiro | dpi.inpe.br/plutao@80/2008/08.19.15.01 |
| 6. Notas | |
| Notas | Setores de Atividade: Pesquisa e desenvolvimento científico. |
| Campos Vazios | alternatejournal archivingpolicy archivist callnumber copyholder copyright creatorhistory descriptionlevel format isbn lineage mark month nextedition number orcid parameterlist parentrepositories previousedition previouslowerunit progress rightsholder schedulinginformation secondarydate secondarykey session shorttitle sponsor subject tertiarymark tertiarytype url |
| 7. Controle da descrição | |
| e-Mail (login) | marcelo.pazos@inpe.br |
| atualizar | |